Denotational semantics.md (3545B)
1 +++ 2 title = 'Denotational semantics' 3 +++ 4 # Denotational semantics 5 ## Compositionality 6 Denotational semantics: defines meaning of each program as mathematical object 7 8 ⟦ ⟧ : syntax → semantics 9 10 Compositionality: meaning of compound statement should be defined in terms of meaning of its components 11 12 An evaluation function on arithmetic expressions is a denotational semantics. 13 14 ## Relational denotational semantics 15 Can represent semantics of imperative program as function from initial state to final state, or as relation between initial and final state. 16 17 Continuing with the WHILE language: 18 19 ```lean 20 def denote : stmt → set (state × state) 21 | stmt.skip := Id 22 | (stmt.assign n a) := {st | prod.snd st = (prod.fst st){n ↦ a (prod.fst st)}} 23 | (stmt.seq S T) := denote S ◯ denote T 24 | (stmt.ite b S T) := (denote S ⇃ b) u (denote T ⇃ (λs, ¬ b s)) 25 | (stmt.while b S) := sorry 26 ``` 27 28 For while, we need a fixpoint. 29 30 ## Fixpoints 31 Fixpoint of `f` is a solution for `X` in the equation `X = f X`. 32 Under some conditions on `f`, unique least and greatest fixpoints will exist. 33 34 For semantics of programming languages: 35 - `X` will have type `set (state × state)`, i.e. `state → state → Prop`, representing relations between states 36 - `f` will be either taking one extra iteration of the loop (if `b` true), or identity (if `b` false) 37 38 Kleene's fixpoint theorem: `f⁰(∅) ∪ f¹(∅) ∪ f²(∅) ∪ ⋯ = lfp f` 39 40 Least fixpoint corresponds to finite executions of a program. 41 42 Inductive predicates correspond to least fixpoints, but are built into Lean's logic. 43 44 ## Monotone functions 45 Take `α, β` types with partial order `≤`. 46 Function `f : α → β` is monotone if `∀a,b: a ≤ b → f a ≤ f b` . 47 48 All monotone functions `f : set α → set α` admit least and greatest fixpoints. 49 50 e.g. `f A = (if A = ∅ then set.univ else ∅)`. 51 Assuming `α` is inhabited, we have `∅ ⊆ set.univ` but `f ∅ = set.univ ⊈ f set.univ` 52 53 ## Complete lattices 54 To define least fixpoint on sets, need `⊆` and `∩`. 55 Complete lattice: ordered type `α` for which each set of type `set α` has an infimum. 56 57 Complete lattice consists of: 58 - partial order `≤ : α → α → Prop` 59 - infimum operator `Inf : set α → α` (kind of like a minimum of a set) 60 - `Inf A` is lower bound of `A`: `Inf A ≤ b` for all `b ∈ A` 61 - `Inf A` is greatest lower bound: `b ≤ Inf A` for all `b` st `∀ a, a ∈ A ≤ a` 62 63 `Inf A` is not necessarily element of `A`. 64 65 Examples: 66 - `set α`: partial order `⊆`, infimum `∩` for all `α` 67 - `Prop`: partial order `→`, infimum `∀` (`Inf A := ∀a ∈ A, a`) 68 - `β → α` if `α` is complete lattice 69 - `α × β` if `α` and `β` are complete lattices 70 71 ## Least fixpoint 72 ```lean 73 def lfp {α : Type} [complete_lattice α] (f : α → α) : α := 74 complete_lattice.Inf ({a | f a ≤ a}) 75 ``` 76 77 Knaster-Tarski theorem: for any monotone function `f`, 78 - `lfp f` is fixpoint, i.e. `lfp f = f (lfp f)` 79 - `lfp f` is smaller than any other fixpoint, i.e. `X = f X → lfp f ≤ X` 80 81 Then, the definition for `while` from [above](#relational-denotational-semantics) is: 82 83 ```lean 84 ... 85 | (stmt.while b S) := lfp (λX, ((denote S ◯ X) ⇃ b) ∪ (Id ⇃ (λs, ¬ b s))) 86 ``` 87 88 ## Application to program equivalence 89 Based on denotational semantics, introduce notion of program equivalence: `S₁ ~ S₂`. 90 91 ```lean 92 def denote_equiv (S₁ S₂ : stmt) : Prop := ⟦S₁⟧ = ⟦S₂⟧ 93 94 infix ` ~ ` := denote_equiv 95 ``` 96 97 Program equivalence can be used to replace subprograms by other subprograms with same semantics.